Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    a__from(X)  → cons(mark(X),from(s(X)))
2:    a__sel(0,cons(X,XS))  → mark(X)
3:    a__sel(s(N),cons(X,XS))  → a__sel(mark(N),mark(XS))
4:    a__minus(X,0)  → 0
5:    a__minus(s(X),s(Y))  → a__minus(mark(X),mark(Y))
6:    a__quot(0,s(Y))  → 0
7:    a__quot(s(X),s(Y))  → s(a__quot(a__minus(mark(X),mark(Y)),s(mark(Y))))
8:    a__zWquot(XS,nil)  → nil
9:    a__zWquot(nil,XS)  → nil
10:    a__zWquot(cons(X,XS),cons(Y,YS))  → cons(a__quot(mark(X),mark(Y)),zWquot(XS,YS))
11:    mark(from(X))  → a__from(mark(X))
12:    mark(sel(X1,X2))  → a__sel(mark(X1),mark(X2))
13:    mark(minus(X1,X2))  → a__minus(mark(X1),mark(X2))
14:    mark(quot(X1,X2))  → a__quot(mark(X1),mark(X2))
15:    mark(zWquot(X1,X2))  → a__zWquot(mark(X1),mark(X2))
16:    mark(cons(X1,X2))  → cons(mark(X1),X2)
17:    mark(s(X))  → s(mark(X))
18:    mark(0)  → 0
19:    mark(nil)  → nil
20:    a__from(X)  → from(X)
21:    a__sel(X1,X2)  → sel(X1,X2)
22:    a__minus(X1,X2)  → minus(X1,X2)
23:    a__quot(X1,X2)  → quot(X1,X2)
24:    a__zWquot(X1,X2)  → zWquot(X1,X2)
There are 31 dependency pairs:
25:    A__FROM(X)  → MARK(X)
26:    A__SEL(0,cons(X,XS))  → MARK(X)
27:    A__SEL(s(N),cons(X,XS))  → A__SEL(mark(N),mark(XS))
28:    A__SEL(s(N),cons(X,XS))  → MARK(N)
29:    A__SEL(s(N),cons(X,XS))  → MARK(XS)
30:    A__MINUS(s(X),s(Y))  → A__MINUS(mark(X),mark(Y))
31:    A__MINUS(s(X),s(Y))  → MARK(X)
32:    A__MINUS(s(X),s(Y))  → MARK(Y)
33:    A__QUOT(s(X),s(Y))  → A__QUOT(a__minus(mark(X),mark(Y)),s(mark(Y)))
34:    A__QUOT(s(X),s(Y))  → A__MINUS(mark(X),mark(Y))
35:    A__QUOT(s(X),s(Y))  → MARK(X)
36:    A__QUOT(s(X),s(Y))  → MARK(Y)
37:    A__ZWQUOT(cons(X,XS),cons(Y,YS))  → A__QUOT(mark(X),mark(Y))
38:    A__ZWQUOT(cons(X,XS),cons(Y,YS))  → MARK(X)
39:    A__ZWQUOT(cons(X,XS),cons(Y,YS))  → MARK(Y)
40:    MARK(from(X))  → A__FROM(mark(X))
41:    MARK(from(X))  → MARK(X)
42:    MARK(sel(X1,X2))  → A__SEL(mark(X1),mark(X2))
43:    MARK(sel(X1,X2))  → MARK(X1)
44:    MARK(sel(X1,X2))  → MARK(X2)
45:    MARK(minus(X1,X2))  → A__MINUS(mark(X1),mark(X2))
46:    MARK(minus(X1,X2))  → MARK(X1)
47:    MARK(minus(X1,X2))  → MARK(X2)
48:    MARK(quot(X1,X2))  → A__QUOT(mark(X1),mark(X2))
49:    MARK(quot(X1,X2))  → MARK(X1)
50:    MARK(quot(X1,X2))  → MARK(X2)
51:    MARK(zWquot(X1,X2))  → A__ZWQUOT(mark(X1),mark(X2))
52:    MARK(zWquot(X1,X2))  → MARK(X1)
53:    MARK(zWquot(X1,X2))  → MARK(X2)
54:    MARK(cons(X1,X2))  → MARK(X1)
55:    MARK(s(X))  → MARK(X)
Consider the SCC {25-55}. The constraints could not be solved.
Tyrolean Termination Tool  (383.35 seconds)   ---  May 3, 2006